Inference at * 1 0 
Iof proof for Lemma neg mul arg bounds:



1. a : 
2. b : 
3. (((-a) * b) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
  ((a * b) < 0)  (((a < 0) & (b > 0))  ((a > 0) & (b < 0))) 

latex

 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{4:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{12:n,
 by PERMUTE{11:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{13:n,
 by PERMUTE{10:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n} 

latex

 1: .....wf..... NILNIL

 1:   ((-a) * b)  
 2: .....wf..... NILNIL

 2:   (-(a * b))  
 3: .....wf..... NILNIL

 3:   0 = 0
 4: .....antecedent..... NILNIL

 4:   True
 5: .....wf..... NILNIL

 5:   ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
 5:   =
 5:   ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
 6: .....wf..... NILNIL

 6: 4. ((((-a) * b) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0))))
 6: 4. =
 6: 4. (((-(a * b)) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0))))
 6:    = 
 7: .....wf..... NILNIL

 7: 3. ((-(a * b)) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
 7:   (-(a * b)) = (-(a * b))
 8: .....wf..... NILNIL

 8: 3. ((-(a * b)) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
 8:   (-0)  
 9: .....wf..... NILNIL

 9: 3. ((-(a * b)) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
 9:   0  
 10: .....antecedent..... NILNIL

 10: 3. ((-(a * b)) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
 10:   True
 11: .....wf..... NILNIL

 11: 3. ((-(a * b)) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
 11:   (-a) = (-a)
 12: .....wf..... NILNIL

 12: 3. ((-(a * b)) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
 12:   (b > 0) = (b > 0)
 13: .....wf..... NILNIL

 13: 3. ((-(a * b)) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
 13:   (b < 0) = (b < 0)
 14: .....wf..... NILNIL

 14: 3. ((-(a * b)) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
 14: 4. (((-(a * b)) > (-0))  ((((-a) > (-0)) & (b > 0))  (((-a) < (-0)) & (b < 0))))
 14: 4. =
 14: 4. (((-(a * b)) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0))))
 14:    = 
 15: 

 15: 3. ((-(a * b)) > (-0))  ((((-a) > (-0)) & (b > 0))  (((-a) < (-0)) & (b < 0)))
 15:   ((a * b) < 0)  (((a < 0) & (b > 0))  ((a > 0) & (b < 0)))
 .

Definitions	left + right, x:A  B(x), {x:A| B(x)} , x:AB(x), Ax, x.A(x), f(a), Type, s = t, a < b, #$n, -n, n * m, i > j, , x:A. B(x), P  Q, t  T, True, T, , P  Q, P & Q, P  Q, P  Q
Lemmas	gt wf, true wf, squash wf, iff wf